(declare-fun x1 () String)
(declare-fun x2 () String)
(declare-fun z1 () String)
(declare-fun z2 () String)
(declare-fun y1 () String)
(declare-fun y2 () String)
(declare-fun t1 () String)
(declare-fun t2 () String)
(assert (= (str.++ (str.++ (str.++ x2 x1) (str.replace (str.++ z2 "fe") (str.++ z1 "gf") "fe")) (str.++ (str.++ y1 t1) y2)) (str.++ z1 (str.++ (str.++ y2 t2) y1))))
(check-sat)
